# HG changeset patch # User wenzelm # Date 864123753 -7200 # Node ID 3e1664348551e8ed9f36d5633de02e62b134cf1c # Parent 067dc2d0748954088ffa0681f126159f7d5e0552 tuned; diff -r 067dc2d07489 -r 3e1664348551 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue May 20 12:14:31 1997 +0200 +++ b/src/HOL/HOL.thy Tue May 20 12:22:33 1997 +0200 @@ -116,6 +116,9 @@ syntax (symbols output) "op ~=" :: ['a, 'a] => bool ("(_ \\/ _)" [51, 51] 50) + "*All" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) + "*Ex" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) + "*Ex1" :: [idts, bool] => bool ("(3\\!_./ _)" [0, 10] 10) syntax (symbols) Not :: bool => bool ("\\ _" [40] 40) @@ -131,12 +134,6 @@ "@case1" :: ['a, 'b] => case_syn ("(2_ \\/ _)" 10) (*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\ _")*) -syntax (symbols output) - "*All" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "*Ex" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "*Ex1" :: [idts, bool] => bool ("(3\\!_./ _)" [0, 10] 10) - - (** Rules and definitions **)