src/Tools/isac/ProgLang/Prog_Expr.thy
changeset 59733 927379190abd
parent 59717 cc83c55e1c1c
child 59773 d88bb023c380
     1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Dec 14 09:41:17 2019 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Dec 14 13:36:40 2019 +0100
     1.3 @@ -93,8 +93,8 @@
     1.4  (**)
     1.5  
     1.6  (*+ for Or_to_List +*)
     1.7 -fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True"; UniversalList)
     1.8 -  | or2list (Const ("HOL.False",_)) = (tracing"### or2list False"; EmptyList)
     1.9 +fun or2list (Const ("HOL.True",_)) = ((*tracing"### or2list True";*) UniversalList)
    1.10 +  | or2list (Const ("HOL.False",_)) = ((*tracing"### or2list False";*) EmptyList)
    1.11    | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
    1.12    | or2list ors =
    1.13      let